(declare-fun ab0c () Bool)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun ab0f () Bool)
(declare-fun ab1aa () Bool)
(declare-fun ab1f () Bool)
(declare-fun ab0aa () Bool)
(declare-fun af () Real)
(declare-fun aab () Real)
(declare-fun ag () Real)
(declare-fun ah () Real)
(declare-fun ai () Real)
(declare-fun aa0aa () Bool)
(declare-fun aa2c () Bool)
(declare-fun aa2aa () Bool)
(declare-fun aa1aa () Bool)
(declare-fun aa3c () Bool)
(declare-fun aa1f () Bool)
(declare-fun aa2f () Bool)
(declare-fun aa0l () Bool)
(declare-fun aa1l () Bool)
(declare-fun j () Real)
(declare-fun aa2l () Bool)
(declare-fun ak () Real)
(declare-fun aa0c () Bool)
(declare-fun aa1c () Bool)
(declare-fun aa3f () Bool)
(declare-fun al () Real)
(declare-fun am () Real)
(declare-fun an () Real)
(declare-fun ao () Real)
(declare-fun aa0f () Bool)
(declare-fun aa3aa () Bool)
(assert (let ((aap (<= al 0.0))) (let ((aaq (not aap))) (let ((aaak aaq)) (let ((aaal (<= 0 j))) (let ((aaam aaal)) (let ((aaan aaak)) (let ((aaao (not aa0l))) (let ((aaap (not aa1l))) (let ((aq (not ab0c))) (let ((aaat (* 2.0 3.0))) (let ((aaau (+ aaat 0.0))) (let ((aaav 0)) (let ((aw (mod aaav (to_int aaau)))) (let ((c (or aa1c))) (let ((aabq (not aa0f))) (let ((bt (not aa1f))) (let ((aabv (not aa2f))) (let ((by (or aa3f))) (let ((aaca (not aa3f))) (let ((aacc (not ab0f))) (let ((aacd (not ab1f))) (let ((aace aacc)) (let ((aacf (not aace))) (let ((ch (= aa1f c))) (let ((aacm ad)) (let ((aacn aacm)) (let ((aacp an)) (let ((aact (distinct ae 0.0))) (let ((aacu (= aab ah))) (let ((aacw (= af ao))) (let ((aacx (and aacu))) (let ((aacy (and aacx))) (let ((aacz (or aacy))) (let ((aada (+ af 0.0))) (let ((aadb (= aada 0.0))) (let ((aadc (or aacf aadb))) (let ((aadd (or aadc))) (let ((aade aacw)) (let ((aar (or aade))) (let ((aadf (and aar aadd))) (let ((aadg (and aadf aacz))) (let ((aadh (<= aab 0.0))) (let ((aadi aadh)) (let ((aas (and aadi))) (let ((dj (or aa0f))) (let ((dk (or aa1f))) (let ((dm (and aa3c))) (let ((dn (and aa2c))) (let ((do (or aa2f))) (let ((dp (xor aa0c false))) (let ((dq (or aaca))) (let ((aads 0)) (let ((aadt (* aads 1.0))) (let ((d (= aadt ah))) (let ((dw (and aas))) (let ((aadz (and aact))) (let ((a (or aadz))) (let ((aaed (and aadg))) (let ((aaee (and aaed))) (let ((aaef (and aaee))) (let ((aaeg (and aaef))) (let ((aaeh (or aacd aaeg))) (let ((aaei (and aaeh))) (let ((aaej (and aaei))) (let ((aaeo (+ aacn 0.0))) (let ((aaep (+ aacp aaeo))) (let ((aaer (>= 0.0 aaep))) (let ((aaet (and aaer))) (let ((fk (or (and (xor aabv false))))) (let ((fm (and (and (xor false (or aabq)))))) (let ((fp (not ab0aa))) (let ((f (= a a))) (let ((fv (= aa2aa a))) (let ((fw (= aa3aa a))) (let ((gp (= ak aab))) (let ((gr (or (= ai an)))) (let ((gu (= ag af))) (and (not (xor (and aaap aaao) (or aa2l aa1l))) (= ai 10.0) (= ak 0.0) (or (not aa3aa) (and (not aa2aa) (not aa1aa))) aaam (<= 0.0 (+ (* 10.0 ai) (+ (* (- 49.0) (* am am)) (- 10.0 (- am))))) (not ab1aa) (= (+ am (mod 0 (to_int af))) 0.0) (= (+ (* 10.0 ai) (* (* (- 49.0) (* am am)) (+ (- 10.0 (- am)) (* (- 10.0) an)))) 0.0) (= aa1aa aa1f) (and (or aa3aa (and (or (or (not aa0aa)))))) (and (and (and aaet))) aaej aaan)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
